\begin{tabbing}
$\forall$${\it the\_w}$:World, $l$:IdLnk, $t$, ${\it t'}$:$\mathbb{N}$.
\\[0ex]($\uparrow$match($l$;$t$;${\it t'}$))
\\[0ex]$\Leftarrow\!\Rightarrow$ \=(($\parallel$snds($l$;$t$)$\parallel$ $\leq$ $\parallel$rcvs($l$;${\it t'}$)$\parallel$)\+
\\[0ex]\& ($\parallel$rcvs($l$;${\it t'}$)$\parallel$ $<$ ($\parallel$snds($l$;$t$)$\parallel$+$\parallel$onlnk($l$;m(source($l$);$t$))$\parallel$)))
\-
\end{tabbing}